\begin{tabbing}
$e$ copies $x$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\exists$$a$:Atom1.\+
\\[0ex](loc($e$) $>>$ $a$ $\Rightarrow$ $x$ when es{-}init(${\it es}$;$e$):vartype(loc($e$);$x$)$>>$$a$)
\\[0ex]\& $\neg$state when $e$$\backslash\backslash$$x$:state@loc($e$)$\backslash\backslash$$x$$>>$$a$
\\[0ex]\& $\neg$$e$ receives $a$
\\[0ex]\& state after $e$$\backslash\backslash$$x$:state@loc($e$)$\backslash\backslash$$x$$>>$$a$
\-
\end{tabbing}